ePMC

Benchmark
Model:consensus v.1 (MDP)
Parameter(s)N = 4, K = 4
Property:steps_min (exp-reward)
Invocation (default)
java -Xms10240m -Xmx10240m -jar ./root/epmc-standard.jar check --model-input-files consensus.4.prism --model-input-type prism --property-input-files consensus.props --property-input-names steps_min --translate-messages false --value-floating-point-output-native true --graphsolver-iterative-stop-criterion relative --graphsolver-iterative-tolerance 1e-6 --const K=4
Execution
Walltime:10.496257781982422s
Return code:0
Relative Error:0.0002465025772942708
Log
assertions-disabled
start-parsing
done-parsing
model-checking
analysing-property steps_min
start-building-explorer
start-building-initial-states-explorer
done-building-initial-states-explorer
done-building-explorer
build-model-start
build-model-states-explored 18448 18447
build-model-done 43136 1
iterating
iterating-progress-unbounded 729 7.143500101057112E-4 1
iterating-progress-unbounded 1525 1.2138258077135184E-4 2
iterating-progress-unbounded 2326 2.475283477627456E-5 3
iterating-progress-unbounded 3127 5.217494870483328E-6 4
iterating-progress-unbounded 3928 1.109787893882705E-6 5
iterating-done 4343 5
model-checking-done 9
command-check-result-is 767.810686020638 steps_min